Search for: All records

Abstract On August 9, 2020, anM_w5.1 earthquake ruptured the uppermost crust near the town of Sparta, North Carolina, creating the first co-seismic faulting surface rupture documented in the Eastern United States. Combining deep learning and matched filter earthquake detection, with differential-travel times relocation, we obtain a catalog of 1761 earthquakes, about 5.8 times the number of events listed in the standard USGS/NEIC catalog. The relocated seismicity revealed a complex fault structure with distinct planar alignments, supported by a moment tensor inversion with significant non-double-couple component. The Sparta mainshock with a centroid depth of 1.3 km is interpreted to have nucleated near the intersection of two main fault strands. The mainshock likely ruptured a blind strike-slip fault and a reverse fault associated with the identified surface rupture, both possibly part of a flower structure-like diffuse fault zone. Our observations highlight a complex behavior of extremely shallow earthquakes in stable continental regions. 

Abstract The 1886 magnitude ∼7 Summerville, South Carolina, earthquake was the largest recorded on the east coast of the United States. A better understanding of this earthquake would allow for an improved evaluation of the intraplate seismic hazard in this region. However, its source fault structure remains unclear. Starting in May 2021, a temporary 19-station short-period seismic network was deployed in the Summerville region. Here, we present our scientific motivation, station geometry, and quality of the recorded seismic data. We also show preliminary results of microearthquake detections and relocations using recordings from both our temporary and four permanent stations in the region. Starting with 52 template events, including two magnitude ∼3 events on 27 September 2021, we perform a matched filter detection with the one year of continuous data, resulting in a catalog of 181 total events. We then determine precise relative locations of a portion of these events using differential travel-time relocation methods, and compare the results with relocation results of 269 events from a previous seismic deployment in 2011–2012. We also determine focal mechanism solutions for three events from 27 September 2021 with magnitudes 2.0, 3.1, and 3.3, and infer their fault planes. Our relocation results show a south-striking west-dipping zone in the southern seismicity cluster, which is consistent with the thrust focal mechanism of the magnitude 3.3 earthquake on 27 September 2021 and results from the previous study based on the temporary deployment in 2011–2012. In comparison, the magnitudes 3.1 and 2.0 events likely occur on a north–south-striking right-lateral strike-slip fault further north, indicating complex patterns of stress and faulting styles in the region. 

Abstract We present the high-resolution Parkfield matched filter relocated earthquake (PKD-MR) catalog for the 2004 Mw 6 Parkfield earthquake sequence in central California. We use high-quality seismic data recorded by the borehole High Resolution Seismic Network combined with matched filter detection and relocations from cross-correlation derived differential travel times. We determine the magnitudes of newly detected events by computing the amplitude ratio between the detections and templates using a principal component fit. The relocated catalog spans from 6 November 2003 to 28 March 2005 and contains 13,914 earthquakes, which is about three times the number of events listed in the Northern California Seismic Network catalog. Our results on the seismicity rate changes before the 2004 mainshock do not show clear precursory signals, although we find an increase in the seismic activity in the creeping section of the San Andreas fault (SAF) (about ∼30 km northwest of the mainshock epicenter) in the weeks prior to the mainshock. We also observe a decrease in the b-value parameter in the Gutenberg–Richter relationship in the creeping section in the weeks prior to the mainshock. Our results suggest stress is increasingly released seismically in the creeping section, accompanied by a decreasing aseismic creeping rate before the mainshock occurrence. However, b-value and seismicity rates remain stable in the Parkfield section where the 2004 mainshock ruptured. This updated catalog can be used to study the evolution of aftershocks and their relations to afterslip following the 2004 Parkfield mainshock, seismicity before the mainshock, and how external stresses interact with the Parkfield section of the SAF and the 2004 sequence. 

SUMMARY We present our estimations and comparisons of the in situ Vp/Vs ratios and seismicity characteristics for the Parkfield segment of the San Andreas fault in northern California and the San Jacinto Fault Zone and its adjacent regions in southern California. Our results show that the high-resolution in situ Vp/Vs ratios are much more complex than the tomographic Vp/Vs models. They show similar variation patterns to those in the tomographic Vp models, indicating that Vp/Vs ratios are controlled by material properties but are also strongly influenced by fluid contents. In Parkfield, we observe velocity contrasts between the creeping and locked sections. In southern California, we see small-scale anomalous Vp/Vs variation patterns, especially where fault segments intersect, terminate and change orientations. In addition, our investigation confirms that the seismicity in Parkfield is more repeatable than in southern California. However, the earthquakes in the southernmost portion of the San Andreas fault, the trifurcation area of the San Jacinto Fault Zone and the Imperial fault are as much likely falling into clusters as those in Parkfield. The correlation of highly similar events with anomalous in situ Vp/Vs ratios supports the important role of fluids in the occurrence of repeating earthquakes. The high-resolution Vp/Vs ratio estimation method and the corresponding results are helpful for revealing roles of fluids in driving earthquake, fault interaction and stress distribution in fault zones. 

Network programmers can currently deploy an arbitrary set of protocols in forwarding devices through data plane programming languages such as P4. However, as any other type of software, P4 programs are subject to bugs and misconfigurations. Network verification tools have been proposed as a means of ensuring that the network behaves as expected, but these tools typically require programmers to manually model P4 programs, are limited in terms of the properties they can guarantee and frequently face severe scalability issues. In this paper, we argue for a novel approach to this problem. Rather than statically inspecting a network configuration looking for bugs, we propose to enforce networking properties at runtime. To this end, we developed P4box, a system for deploying runtime monitors in programmable data planes. Our results show that P4box allows programmers to easily express a broad range of properties. Moreover, we demonstrate that runtime monitors represent a small overhead to network devices in terms of latency and resource consumption. 

Recent trends in software-defined networking have extended network programmability to the data plane. Unfortunately, the chance of introducing bugs increases significantly. Verification can help prevent bugs by assuring that the program does not violate its requirements. Although research on the verification of P4 programs is very active, we still need tools to make easier for programmers to express properties and to rapidly verify complex invariants. In this paper, we leverage assertions and symbolic execution to propose a more general P4 verification approach. Developers annotate P4 programs with assertions expressing general network correctness properties; the result is transformed into C models and all possible paths symbolically executed. We implement a prototype, and use it to show the feasibility of the verification approach. Because symbolic execution does not scale well, we investigate a set of techniques to speed up the process for the specific case of P4 programs. We use the prototype implemented to show the gains provided by three speed up techniques (use of constraints, program slicing, parallelization), and experiment with different compiler optimization choices. We show our tool can uncover a broad range of bugs, and can do it in less than a minute considering various P4 applications. 

Program synthesis is the problem of finding a program that satisfies a given specification. Most program synthesizers are based on enumerating program candidates that satisfy the specification. Recently, several new tools for program synthesis have been proposed where Satisfiability Modulo Theories (SMT) solvers are used to prune the search space by discarding programs that do not satisfy the specification. The size of current tree-based SMT encodings for program synthesis grows exponentially with the size of the program. In this paper, a new compact line-based encoding is proposed that allows a faster enumeration of the program space. Experimental results on a large set of query synthesis problem instances show that using the new encoding results in a more effective tool that is able to synthesize larger programs. 

Recent trends in software-defined networking have extended network programmability to the data plane through programming languages such as P4. Unfortunately, the chance of introducing bugs in the network also increases significantly in this new context. Existing data plane verification approaches are unable to model P4 programs, or they present severe restrictions in the set of properties that can be modeled. In this paper, we introduce a data plane program verification approach based on assertion checking and symbolic execution. Network programmers annotate P4 programs with assertions expressing general security and correctness properties. Once annotated, these programs are transformed into C-based models and all their possible paths are symbolically executed. Results show that the proposed approach, called ASSERT-P4, can uncover a broad range of bugs and software flaws. Furthermore, experimental evaluation shows that it takes less than a minute for verifying various P4 applications proposed in the literature.